AXIOM COND1
(∀ P) (∀ X) (∀ Y) (P⊃IF P THEN X ELSE Y=X) 

AXIOM COND2
(∀ P) (∀ X) (∀ Y) (¬ P⊃IF P THEN X ELSE Y=Y) 

AXIOM TRUE1
TRUE 

AXIOM TRUE2
(∀ P) (P=TRUE≡P) 

AXIOM REFLEX
(∀ X) (X=X) 

AXIOM SYMEQ
(∀ X) (∀ Y) (X=Y⊃Y=X) 

AXIOM TRANSEQ
(∀ X) (∀ Y) (∀ Z) (X=Y∧Y=Z⊃X=Z) 

AXIOM NOTEQ
(∀ X) (∀ Y) (XNEQY≡¬ (X=Y)) 

PROOF ONE 

1:	IF P THEN IF P THEN A ELSE B ELSE C=IF P THEN IF P THEN A 
ELSE B ELSE C BY AXIOM(REFLEX,IF P THEN IF P THEN A ELSE B ELSE C) 

2:	P⊃IF P THEN A ELSE B=A BY AXIOM(COND1,P,A,B) 

3:	P BY ASSUMPTION 

4:	IF P THEN A ELSE B=A BY MP(2,3) ASSUMING (3) 

5:	IF P THEN IF P THEN A ELSE B ELSE C=IF P THEN A ELSE C BY 
REPL(1,4,2) ASSUMING (3) 

6:	¬ P⊃IF P THEN A ELSE C=C BY AXIOM(COND2,P,A,C) 

7:	¬ P⊃IF P THEN IF P THEN A ELSE B ELSE C=C BY AXIOM(COND2,P,IF
 P THEN A ELSE B,C) 

8:	¬ P BY ASSUMPTION 

9:	IF P THEN A ELSE C=C BY MP(6,8) ASSUMING (8) 

10:	IF P THEN IF P THEN A ELSE B ELSE C=C BY MP(7,8) ASSUMING (8)~
 

11:	IF P THEN IF P THEN A ELSE B ELSE C=IF P THEN A ELSE C BY 
REPR(10,9,2) ASSUMING (8) 

12:	P∨¬ P BY TAUT (P∨¬ P) 

13:	P⊃IF P THEN IF P THEN A ELSE B ELSE C=IF P THEN A ELSE C BY 
DED(5,3) 

14:	¬ P⊃IF P THEN IF P THEN A ELSE B ELSE C=IF P THEN A ELSE C BY~
 DED(11,8) 

15:	IF P THEN IF P THEN A ELSE B ELSE C=IF P THEN A ELSE C BY OE(
12,13,14) 

16:	(∀ B) (∀ A) (∀ P) (IF P THEN IF P THEN A ELSE B ELSE C=IF P 
THEN A ELSE C) BY UG(15,P,A,B)